Исследование возможности разработки безмасочного рентгеновского нанолитографа для формирования наноструктур с размерами от 13 нм и ниже на базе синхротронного и/или плазменного источника.
И насколько я знаю, там и с готовым фотолитографом надо ещё много чего из оборудования.
Королёву еще относительно повезло. Там двоих из того института по этому делу расстреляли, а жену одного из них отправили в ссылку, как жену шпиона (как это ложится в версию наказания за расстрату не понятно).
В любом случае, если что-то похожее начнется в наши дни по отношению к инжинерам, то придётся закрывать границы, чтобы не убежали. А в университеты набирать в принудительном порядке по спискам, а то добровольно ни кто не пойдет.
Вроде лет пять назад, СО РАН выражало готовность сделать EUV степпер на основе ускорителя. Не знаю, в чем там дело встало, в тех. проблемах или из-за финансирования.
А как вы определили что он "Лахтинский кремлебот"? Я так-же не поддерживаю его комментарий, но остальные 6 его комментариев вполне осмыслены и без политики.
Приходилось что-то подобное делать. Правда, не было гарантии что на сайте отображается реальное наличие, гарантированная проверка остатков производилась при резервировании в момент заказа. Бизнес устроил такой компромисс.
Только, если сильный ИИ будет осознавать как работает его базовый алгоритм или ещё хуже — сможет его модифицировать, он не будет работать стабильно. Примерно как не может стабильно существовать человек получивший прямой доступ к своей гормональной системе, т.е. наркоман или психбольной. Есть вероятность, что лучше интеллекта способного к самоосознанию чем у текущего хомо-сапиенса в принципе быть не может. Посмотрите, какие проблемы уже сейчас испытывает человек со своими мозгами: депрессии на ровном месте, самоубийства, психические заболевания.
В общем виде — разумеется невозможно. Там еще Теорема Гёделя нам рукой машет. Но, ведь значительное количество программ содержат очень простую арифметику, там нет ни каких полиномов с большими степенями…
Доказать _уже_ написанную (без оглядки на способ доказательства) программу на языке общего назначения (скажем, Java), как правило, нереально.
Вот я и мел в виду. Что почему бы средствами ASP например, парсить такие программы на языке общего назначения и создавая логическую модель — автоматически доказывать ее корректность. Например, отвечая на вопросы — при каких наборах входных параметров программа будет падать в необрабатываемые исключения (деление на ноль допустим).
Эм… ну это я Вас хотел спросить, бывает ли такое )
Возможно будет коряво, но представляю себе это так:
Например допустим, я написал свою СУБД (со своими блэкджеками и ш алгоритмами) и мне нужно верифицировать, будет ли соблюдаться гарантированная изолированность транзакций. Во всех комбинациях возможных запросов SQL с учетом параллельного асинхронного их выполнения. Я просто “скармливаю” этот код системе верификации и она выдает ответ – да, транзакции всегда будут изолированными при любых запросах или наоборот – нет не будут, из за такого то участка в коде.
С автогенерацией кода на основе логической модели – сложнее, но я где то слышал, что в узких областях экспериментировали с этим.
Возможно, это мечта ленивого наивного программиста, но: что мешает использовать LP в авто-генерации готового кода? Например, на Java или хотя бы его тестирование(или верификация).
Когда молодые ученые станут академиками, то у них заберут зарплату и отдадут молодым ученым.
Разумеется нет. Там только:
И насколько я знаю, там и с готовым фотолитографом надо ещё много чего из оборудования.
Вроде как НИР открыли на безмасочные 14нм. Но вилами по воде это пока конечно. https://www.roseltorg.ru/procedure/0173100009521000167
Не понятно тогда, как они выиграли тендер с Иволгой на 900млн $ в Аргентину.
Надеюсь, хотя бы часть вырученных денег пойдет на развитие.
Королёву еще относительно повезло. Там двоих из того института по этому делу расстреляли, а жену одного из них отправили в ссылку, как жену шпиона (как это ложится в версию наказания за расстрату не понятно).
В любом случае, если что-то похожее начнется в наши дни по отношению к инжинерам, то придётся закрывать границы, чтобы не убежали. А в университеты набирать в принудительном порядке по спискам, а то добровольно ни кто не пойдет.
Вроде лет пять назад, СО РАН выражало готовность сделать EUV степпер на основе ускорителя. Не знаю, в чем там дело встало, в тех. проблемах или из-за финансирования.
Вот здесь ещё Сергей Попов пытается популярно рассказать об этом.
https://www.youtube.com/watch?v=HoyfXXJ6x_A
А как вы определили что он "Лахтинский кремлебот"? Я так-же не поддерживаю его комментарий, но остальные 6 его комментариев вполне осмыслены и без политики.
Мне кажется, в оценке управления большими проектами вы заняли крайнюю предвзятую позицию. Впрочем, отчасти я с вами согласен.
Вы такой маркетинг сейчас загубили..
Нашел их курс лекций https://studfile.net/preview/876206/
Пробежался по диагонали, на мой взгляд, как-то поверхностно, на уровне базового курса по макро-микроэкономике. Возможно это не то.
Приходилось что-то подобное делать. Правда, не было гарантии что на сайте отображается реальное наличие, гарантированная проверка остатков производилась при резервировании в момент заказа. Бизнес устроил такой компромисс.
А если в качестве учредительных взносов в бизнес — партнёры вносят интеллектуальную собственность(идеи) и свое рабочее время, на этапе стартапа?
Только, если сильный ИИ будет осознавать как работает его базовый алгоритм или ещё хуже — сможет его модифицировать, он не будет работать стабильно. Примерно как не может стабильно существовать человек получивший прямой доступ к своей гормональной системе, т.е. наркоман или психбольной. Есть вероятность, что лучше интеллекта способного к самоосознанию чем у текущего хомо-сапиенса в принципе быть не может. Посмотрите, какие проблемы уже сейчас испытывает человек со своими мозгами: депрессии на ровном месте, самоубийства, психические заболевания.
Вот я и мел в виду. Что почему бы средствами ASP например, парсить такие программы на языке общего назначения и создавая логическую модель — автоматически доказывать ее корректность. Например, отвечая на вопросы — при каких наборах входных параметров программа будет падать в необрабатываемые исключения (деление на ноль допустим).
Возможно будет коряво, но представляю себе это так:
Например допустим, я написал свою СУБД (со своими
блэкджеками и шалгоритмами) и мне нужно верифицировать, будет ли соблюдаться гарантированная изолированность транзакций. Во всех комбинациях возможных запросов SQL с учетом параллельного асинхронного их выполнения. Я просто “скармливаю” этот код системе верификации и она выдает ответ – да, транзакции всегда будут изолированными при любых запросах или наоборот – нет не будут, из за такого то участка в коде.С автогенерацией кода на основе логической модели – сложнее, но я где то слышал, что в узких областях экспериментировали с этим.